This disclosure describes the verification of complex circuit designs using a novel approach. The capability of Sequential Equivalence Checking (SEC) tools is enhanced by designing a process with the weaknesses of SEC tools in mind.
SEC is a PSPACE-complete problem, meaning that the best possible algorithms have exponential run times in the worst case; hence, SEC tools can be expected to run into capacity issues frequently. Yet the power of these tools is immense as they allow verifying sequential optimizations of complex designs with a confidence that cannot be achieved using traditional simulation-based verification. The process described in this disclosure is scalable and can be used to verify much more complex designs than would otherwise be possible, provided the majority of the logic edits can be verified in a stand-alone manner and logic edits that need to be promoted to higher levels of hierarchy are minimal.
Intrinsity, Inc, (Intrinsity), the assignee of this disclosure, is a fabless semiconductor company whose operations include optimizing a customer's RTL (Register Transfer Level) code. Optimizations for higher speed and/or lower power are achieved either by changing the existing RTL, or by re-implementing portions of the design in different types of logic. The design is verified with simulation and formal verification tools.
SEC, a type of formal verification tool, has a lower processing capacity than required for current and future complex designs. By breaking the problem of sequentially verifying a circuit into a series of steps, larger circuits can be verified than would otherwise be possible.
For formal verification, conventional combinational logical equivalence checking (LEC) is usually not possible due to the types of logic changes being made. Combinational LEC tools require a one-to-one correspondence between the state holding elements (flops and latches) of the two designs. Some examples of changes that break this correspondence include:
1 Retiming by moving logic across latch boundaries
2. Recoding of state machines
3. Clock gating
4. Pipeline stage insertion/removal
5. Resource Allocation
SEC differs from regular combinational LEC in that sequential elements in the design are not assumed to correspond. Thus, for the types of changes described above, SEC can be used to prove equivalence of designs that LEC would not be able to prove. The trade off is that SEC algorithms are more difficult and require greater computational resources than regular LEC algorithms.
For SEC, the computational resources needed to prove equivalence between two integrated circuits is exponentially related to the size of the integrated circuit as well as the number and type of logic changes between the semiconductor designs. Thus, formally proving the reference RTL equivalent to the design for a large design, or a design with multiple complex changes, can easily create a problem beyond the capacity of current SEC tools. Sequential equivalence checking is an active area of research.
Several techniques simplify the problems presented for formally verifying larger semiconductor designs:                1. Limiting the number of logic changes or edits being proven at any one time. While this technique would be obvious to anyone skilled in the art, the novelty of our method involves organizing these edits to automate checking so that dependent edits are not checked until after those edits upon which they depend.        2. Dividing or partitioning the semiconductor design into smaller sub-blocks that are more easily handled by the tools. Although this technique would also be obvious to anyone skilled in the art, the novelty of our method is being able to determine automatically whether the partition chosen in which to verify a group of edits might result in a false pass of equivalence.        3. Using black boxes to limit the amount of logic that needs to be considered by the verification tool. This use of black boxes is a well-known technique. The novelty of our method is in associating a set of black box modules with individual groups of edits and verifying that the use of such black boxes does not introduce any false passes.        4. Using input constraints when verifying within a partition that does not constitute the entire design. Without input constraints, some circuits may not prove to be equivalent because they differ under input combinations that are unrealizable within the design. Note that using an input constraint creates a proof obligation to verify that the constraint is upheld within an enclosing partition. The use of input constraints for verifying partial designs is a well-known technique. The novelty of our method comes from enforcing the obligation of proving input constraints within some enclosing module that generates the constrained inputs to prevent reporting a false pass.        
The solution presented in this disclosure combines these methods, resulting in simpler problems to be solved by the sequential equivalence checker. These techniques scale well with the size of the semiconductor design.
However, these techniques also leave room for human error that can invalidate the overall proof of equivalence. The major purpose of this invention is to create a method that eliminates the sources of human error that would invalidate the overall proof. Here are some sources of human error:                1 Failure to do equivalence checking for every group of edits.        2. Attempting to prove an edit without having the prerequisite conditions for the edit to become effective.        3. Attempting to prove an edit within a partition that does not contain all the modules affected by it.        4. Attempting to use as a black box a module which is affected by the edit being proved.        5. Failure to verify that the reference design is equivalent to the modified design with all edits disabled.        6 Failure to prove that all input constraints for a partition are upheld within its enclosing partition.        